#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include "literal.h"

namespace solver {

	class clause
	{
	public:

		// TODO: because clause is not the one being "searched", we can 
		// go ahead and turn this into something smaller like a normal vector
		std::vector<literal> literals;

		int line_number;

		void clear()
		{
			literals.clear();
		}

		bool operator==(clause& c)
		{
			int s = literals.size();
			int cs = c.literals.size();
			if (cs != s)
				return false;
			for (int i = 0; i < s; i++)
			{
				if (literals[i] != c.literals[i])
					return false;
			}
			return true;
		}

		bool operator!=(clause& c)
		{
			return !(*this == c);
		}

	};

}
